(set-info :smt-lib-version 2.6)
(set-logic QF_UF)
(set-info :source |
CADE ATP System competition. See http://www.cs.miami.edu/~tptp/CASC
 for more information. 

This benchmark was obtained by trying to find a finite model of a first-order 
formula (Albert Oliveras).
|)
(set-info :category "crafted")
(set-info :status unsat)
(declare-sort U 0)
(declare-fun c14 () U)
(declare-fun c12 () U)
(declare-fun p4 (U U) Bool)
(declare-fun c13 () U)
(declare-fun p3 (U U) Bool)
(declare-fun c15 () U)
(declare-fun c17 () U)
(declare-fun p6 (U U) Bool)
(declare-fun p2 (U U) Bool)
(declare-fun p1 (U U) Bool)
(declare-fun c11 () U)
(declare-fun f5 (U U) U)
(declare-fun c10 () U)
(declare-fun p8 (U) Bool)
(declare-fun c16 () U)
(declare-fun p9 (U U) Bool)
(declare-fun p7 (U U) Bool)
(declare-fun c_0 () U)
(declare-fun c_1 () U)
(declare-fun c_2 () U)
(declare-fun c_3 () U)
(declare-fun c_4 () U)
(assert (let ((?v_80 (= c_0 c_0))) (let ((?v_25 (not ?v_80)) (?v_50 (p3 c_0 c_0)) (?v_83 (= c_0 c_1))) (let ((?v_26 (not ?v_83)) (?v_51 (p3 c_0 c_1)) (?v_86 (= c_0 c_2))) (let ((?v_27 (not ?v_86)) (?v_52 (p3 c_0 c_2)) (?v_89 (= c_0 c_3))) (let ((?v_28 (not ?v_89)) (?v_53 (p3 c_0 c_3)) (?v_92 (= c_0 c_4))) (let ((?v_29 (not ?v_92)) (?v_54 (p3 c_0 c_4)) (?v_95 (= c_1 c_0))) (let ((?v_30 (not ?v_95)) (?v_55 (p3 c_1 c_0)) (?v_98 (= c_1 c_1))) (let ((?v_31 (not ?v_98)) (?v_56 (p3 c_1 c_1)) (?v_101 (= c_1 c_2))) (let ((?v_32 (not ?v_101)) (?v_57 (p3 c_1 c_2)) (?v_104 (= c_1 c_3))) (let ((?v_33 (not ?v_104)) (?v_58 (p3 c_1 c_3)) (?v_107 (= c_1 c_4))) (let ((?v_34 (not ?v_107)) (?v_59 (p3 c_1 c_4)) (?v_110 (= c_2 c_0))) (let ((?v_35 (not ?v_110)) (?v_60 (p3 c_2 c_0)) (?v_113 (= c_2 c_1))) (let ((?v_36 (not ?v_113)) (?v_61 (p3 c_2 c_1)) (?v_116 (= c_2 c_2))) (let ((?v_37 (not ?v_116)) (?v_62 (p3 c_2 c_2)) (?v_119 (= c_2 c_3))) (let ((?v_38 (not ?v_119)) (?v_63 (p3 c_2 c_3)) (?v_122 (= c_2 c_4))) (let ((?v_39 (not ?v_122)) (?v_64 (p3 c_2 c_4)) (?v_125 (= c_3 c_0))) (let ((?v_40 (not ?v_125)) (?v_65 (p3 c_3 c_0)) (?v_128 (= c_3 c_1))) (let ((?v_41 (not ?v_128)) (?v_66 (p3 c_3 c_1)) (?v_131 (= c_3 c_2))) (let ((?v_42 (not ?v_131)) (?v_67 (p3 c_3 c_2)) (?v_134 (= c_3 c_3))) (let ((?v_43 (not ?v_134)) (?v_68 (p3 c_3 c_3)) (?v_137 (= c_3 c_4))) (let ((?v_44 (not ?v_137)) (?v_69 (p3 c_3 c_4)) (?v_140 (= c_4 c_0))) (let ((?v_45 (not ?v_140)) (?v_70 (p3 c_4 c_0)) (?v_143 (= c_4 c_1))) (let ((?v_46 (not ?v_143)) (?v_71 (p3 c_4 c_1)) (?v_146 (= c_4 c_2))) (let ((?v_47 (not ?v_146)) (?v_72 (p3 c_4 c_2)) (?v_149 (= c_4 c_3))) (let ((?v_48 (not ?v_149)) (?v_73 (p3 c_4 c_3)) (?v_152 (= c_4 c_4))) (let ((?v_49 (not ?v_152)) (?v_74 (p3 c_4 c_4)) (?v_81 (p4 c_0 c_0))) (let ((?v_0 (not ?v_81)) (?v_84 (p4 c_0 c_1))) (let ((?v_2 (not ?v_84)) (?v_96 (p4 c_1 c_0))) (let ((?v_1 (not ?v_96)) (?v_87 (p4 c_0 c_2))) (let ((?v_5 (not ?v_87)) (?v_111 (p4 c_2 c_0))) (let ((?v_4 (not ?v_111)) (?v_90 (p4 c_0 c_3))) (let ((?v_10 (not ?v_90)) (?v_126 (p4 c_3 c_0))) (let ((?v_9 (not ?v_126)) (?v_93 (p4 c_0 c_4))) (let ((?v_17 (not ?v_93)) (?v_141 (p4 c_4 c_0))) (let ((?v_16 (not ?v_141)) (?v_99 (p4 c_1 c_1))) (let ((?v_3 (not ?v_99)) (?v_102 (p4 c_1 c_2))) (let ((?v_7 (not ?v_102)) (?v_114 (p4 c_2 c_1))) (let ((?v_6 (not ?v_114)) (?v_105 (p4 c_1 c_3))) (let ((?v_12 (not ?v_105)) (?v_129 (p4 c_3 c_1))) (let ((?v_11 (not ?v_129)) (?v_108 (p4 c_1 c_4))) (let ((?v_19 (not ?v_108)) (?v_144 (p4 c_4 c_1))) (let ((?v_18 (not ?v_144)) (?v_117 (p4 c_2 c_2))) (let ((?v_8 (not ?v_117)) (?v_120 (p4 c_2 c_3))) (let ((?v_14 (not ?v_120)) (?v_132 (p4 c_3 c_2))) (let ((?v_13 (not ?v_132)) (?v_123 (p4 c_2 c_4))) (let ((?v_21 (not ?v_123)) (?v_147 (p4 c_4 c_2))) (let ((?v_20 (not ?v_147)) (?v_135 (p4 c_3 c_3))) (let ((?v_15 (not ?v_135)) (?v_138 (p4 c_3 c_4))) (let ((?v_23 (not ?v_138)) (?v_150 (p4 c_4 c_3))) (let ((?v_22 (not ?v_150)) (?v_153 (p4 c_4 c_4))) (let ((?v_24 (not ?v_153)) (?v_82 (p2 c_0 c_0)) (?v_97 (p2 c_1 c_0)) (?v_112 (p2 c_2 c_0)) (?v_127 (p2 c_3 c_0)) (?v_142 (p2 c_4 c_0)) (?v_85 (p2 c_0 c_1)) (?v_100 (p2 c_1 c_1)) (?v_115 (p2 c_2 c_1)) (?v_130 (p2 c_3 c_1)) (?v_145 (p2 c_4 c_1)) (?v_88 (p2 c_0 c_2)) (?v_103 (p2 c_1 c_2)) (?v_118 (p2 c_2 c_2)) (?v_133 (p2 c_3 c_2)) (?v_148 (p2 c_4 c_2)) (?v_91 (p2 c_0 c_3)) (?v_106 (p2 c_1 c_3)) (?v_121 (p2 c_2 c_3)) (?v_136 (p2 c_3 c_3)) (?v_151 (p2 c_4 c_3)) (?v_94 (p2 c_0 c_4)) (?v_109 (p2 c_1 c_4)) (?v_124 (p2 c_2 c_4)) (?v_139 (p2 c_3 c_4)) (?v_154 (p2 c_4 c_4)) (?v_155 (p1 c_0 c_0)) (?v_156 (p1 c_0 c_1)) (?v_157 (p1 c_0 c_2)) (?v_158 (p1 c_0 c_3)) (?v_159 (p1 c_0 c_4)) (?v_160 (p1 c_1 c_0)) (?v_161 (p1 c_1 c_1)) (?v_162 (p1 c_1 c_2)) (?v_163 (p1 c_1 c_3)) (?v_164 (p1 c_1 c_4)) (?v_165 (p1 c_2 c_0)) (?v_166 (p1 c_2 c_1)) (?v_167 (p1 c_2 c_2)) (?v_168 (p1 c_2 c_3)) (?v_169 (p1 c_2 c_4)) (?v_170 (p1 c_3 c_0)) (?v_171 (p1 c_3 c_1)) (?v_172 (p1 c_3 c_2)) (?v_173 (p1 c_3 c_3)) (?v_174 (p1 c_3 c_4)) (?v_175 (p1 c_4 c_0)) (?v_176 (p1 c_4 c_1)) (?v_177 (p1 c_4 c_2)) (?v_178 (p1 c_4 c_3)) (?v_179 (p1 c_4 c_4)) (?v_181 (f5 c_0 c_0)) (?v_75 (not (p8 c_0))) (?v_180 (p6 c_0 c_0)) (?v_183 (f5 c_0 c_1)) (?v_182 (p6 c_0 c_1)) (?v_185 (f5 c_0 c_2)) (?v_184 (p6 c_0 c_2)) (?v_187 (f5 c_0 c_3)) (?v_186 (p6 c_0 c_3)) (?v_189 (f5 c_0 c_4)) (?v_188 (p6 c_0 c_4)) (?v_191 (f5 c_1 c_0)) (?v_76 (not (p8 c_1))) (?v_190 (p6 c_1 c_0)) (?v_193 (f5 c_1 c_1)) (?v_192 (p6 c_1 c_1)) (?v_195 (f5 c_1 c_2)) (?v_194 (p6 c_1 c_2)) (?v_197 (f5 c_1 c_3)) (?v_196 (p6 c_1 c_3)) (?v_199 (f5 c_1 c_4)) (?v_198 (p6 c_1 c_4)) (?v_201 (f5 c_2 c_0)) (?v_77 (not (p8 c_2))) (?v_200 (p6 c_2 c_0)) (?v_203 (f5 c_2 c_1)) (?v_202 (p6 c_2 c_1)) (?v_205 (f5 c_2 c_2)) (?v_204 (p6 c_2 c_2)) (?v_207 (f5 c_2 c_3)) (?v_206 (p6 c_2 c_3)) (?v_209 (f5 c_2 c_4)) (?v_208 (p6 c_2 c_4)) (?v_211 (f5 c_3 c_0)) (?v_78 (not (p8 c_3))) (?v_210 (p6 c_3 c_0)) (?v_213 (f5 c_3 c_1)) (?v_212 (p6 c_3 c_1)) (?v_215 (f5 c_3 c_2)) (?v_214 (p6 c_3 c_2)) (?v_217 (f5 c_3 c_3)) (?v_216 (p6 c_3 c_3)) (?v_219 (f5 c_3 c_4)) (?v_218 (p6 c_3 c_4)) (?v_221 (f5 c_4 c_0)) (?v_79 (not (p8 c_4))) (?v_220 (p6 c_4 c_0)) (?v_223 (f5 c_4 c_1)) (?v_222 (p6 c_4 c_1)) (?v_225 (f5 c_4 c_2)) (?v_224 (p6 c_4 c_2)) (?v_227 (f5 c_4 c_3)) (?v_226 (p6 c_4 c_3)) (?v_229 (f5 c_4 c_4)) (?v_228 (p6 c_4 c_4))) (let ((?v_230 (not ?v_82)) (?v_235 (not ?v_97)) (?v_240 (not ?v_112)) (?v_245 (not ?v_127)) (?v_250 (not ?v_142)) (?v_231 (not ?v_85)) (?v_236 (not ?v_100)) (?v_241 (not ?v_115)) (?v_246 (not ?v_130)) (?v_251 (not ?v_145)) (?v_232 (not ?v_88)) (?v_237 (not ?v_103)) (?v_242 (not ?v_118)) (?v_247 (not ?v_133)) (?v_252 (not ?v_148)) (?v_233 (not ?v_91)) (?v_238 (not ?v_106)) (?v_243 (not ?v_121)) (?v_248 (not ?v_136)) (?v_253 (not ?v_151)) (?v_234 (not ?v_94)) (?v_239 (not ?v_109)) (?v_244 (not ?v_124)) (?v_249 (not ?v_139)) (?v_254 (not ?v_154)) (?v_255 (p9 c_0 c_0))) (let ((?v_330 (not ?v_255)) (?v_305 (p7 c_0 c_0))) (let ((?v_256 (not ?v_305)) (?v_257 (p9 c_0 c_1))) (let ((?v_331 (not ?v_257)) (?v_306 (p7 c_0 c_1))) (let ((?v_258 (not ?v_306)) (?v_259 (p9 c_0 c_2))) (let ((?v_332 (not ?v_259)) (?v_307 (p7 c_0 c_2))) (let ((?v_260 (not ?v_307)) (?v_261 (p9 c_0 c_3))) (let ((?v_333 (not ?v_261)) (?v_308 (p7 c_0 c_3))) (let ((?v_262 (not ?v_308)) (?v_263 (p9 c_0 c_4))) (let ((?v_334 (not ?v_263)) (?v_309 (p7 c_0 c_4))) (let ((?v_264 (not ?v_309)) (?v_265 (p9 c_1 c_0))) (let ((?v_335 (not ?v_265)) (?v_310 (p7 c_1 c_0))) (let ((?v_266 (not ?v_310)) (?v_267 (p9 c_1 c_1))) (let ((?v_336 (not ?v_267)) (?v_311 (p7 c_1 c_1))) (let ((?v_268 (not ?v_311)) (?v_269 (p9 c_1 c_2))) (let ((?v_337 (not ?v_269)) (?v_312 (p7 c_1 c_2))) (let ((?v_270 (not ?v_312)) (?v_271 (p9 c_1 c_3))) (let ((?v_338 (not ?v_271)) (?v_313 (p7 c_1 c_3))) (let ((?v_272 (not ?v_313)) (?v_273 (p9 c_1 c_4))) (let ((?v_339 (not ?v_273)) (?v_314 (p7 c_1 c_4))) (let ((?v_274 (not ?v_314)) (?v_275 (p9 c_2 c_0))) (let ((?v_340 (not ?v_275)) (?v_315 (p7 c_2 c_0))) (let ((?v_276 (not ?v_315)) (?v_277 (p9 c_2 c_1))) (let ((?v_341 (not ?v_277)) (?v_316 (p7 c_2 c_1))) (let ((?v_278 (not ?v_316)) (?v_279 (p9 c_2 c_2))) (let ((?v_342 (not ?v_279)) (?v_317 (p7 c_2 c_2))) (let ((?v_280 (not ?v_317)) (?v_281 (p9 c_2 c_3))) (let ((?v_343 (not ?v_281)) (?v_318 (p7 c_2 c_3))) (let ((?v_282 (not ?v_318)) (?v_283 (p9 c_2 c_4))) (let ((?v_344 (not ?v_283)) (?v_319 (p7 c_2 c_4))) (let ((?v_284 (not ?v_319)) (?v_285 (p9 c_3 c_0))) (let ((?v_345 (not ?v_285)) (?v_320 (p7 c_3 c_0))) (let ((?v_286 (not ?v_320)) (?v_287 (p9 c_3 c_1))) (let ((?v_346 (not ?v_287)) (?v_321 (p7 c_3 c_1))) (let ((?v_288 (not ?v_321)) (?v_289 (p9 c_3 c_2))) (let ((?v_347 (not ?v_289)) (?v_322 (p7 c_3 c_2))) (let ((?v_290 (not ?v_322)) (?v_291 (p9 c_3 c_3))) (let ((?v_348 (not ?v_291)) (?v_323 (p7 c_3 c_3))) (let ((?v_292 (not ?v_323)) (?v_293 (p9 c_3 c_4))) (let ((?v_349 (not ?v_293)) (?v_324 (p7 c_3 c_4))) (let ((?v_294 (not ?v_324)) (?v_295 (p9 c_4 c_0))) (let ((?v_350 (not ?v_295)) (?v_325 (p7 c_4 c_0))) (let ((?v_296 (not ?v_325)) (?v_297 (p9 c_4 c_1))) (let ((?v_351 (not ?v_297)) (?v_326 (p7 c_4 c_1))) (let ((?v_298 (not ?v_326)) (?v_299 (p9 c_4 c_2))) (let ((?v_352 (not ?v_299)) (?v_327 (p7 c_4 c_2))) (let ((?v_300 (not ?v_327)) (?v_301 (p9 c_4 c_3))) (let ((?v_353 (not ?v_301)) (?v_328 (p7 c_4 c_3))) (let ((?v_302 (not ?v_328)) (?v_303 (p9 c_4 c_4))) (let ((?v_354 (not ?v_303)) (?v_329 (p7 c_4 c_4))) (let ((?v_304 (not ?v_329))) (and (distinct c_0 c_1 c_2 c_3 c_4) (p4 c14 c12) (p4 c14 c13) (or ?v_25 ?v_50) (or ?v_26 ?v_51) (or ?v_27 ?v_52) (or ?v_28 ?v_53) (or ?v_29 ?v_54) (or ?v_30 ?v_55) (or ?v_31 ?v_56) (or ?v_32 ?v_57) (or ?v_33 ?v_58) (or ?v_34 ?v_59) (or ?v_35 ?v_60) (or ?v_36 ?v_61) (or ?v_37 ?v_62) (or ?v_38 ?v_63) (or ?v_39 ?v_64) (or ?v_40 ?v_65) (or ?v_41 ?v_66) (or ?v_42 ?v_67) (or ?v_43 ?v_68) (or ?v_44 ?v_69) (or ?v_45 ?v_70) (or ?v_46 ?v_71) (or ?v_47 ?v_72) (or ?v_48 ?v_73) (or ?v_49 ?v_74) (or ?v_0 ?v_0) (or ?v_2 ?v_1) (or ?v_5 ?v_4) (or ?v_10 ?v_9) (or ?v_17 ?v_16) (or ?v_1 ?v_2) (or ?v_3 ?v_3) (or ?v_7 ?v_6) (or ?v_12 ?v_11) (or ?v_19 ?v_18) (or ?v_4 ?v_5) (or ?v_6 ?v_7) (or ?v_8 ?v_8) (or ?v_14 ?v_13) (or ?v_21 ?v_20) (or ?v_9 ?v_10) (or ?v_11 ?v_12) (or ?v_13 ?v_14) (or ?v_15 ?v_15) (or ?v_23 ?v_22) (or ?v_16 ?v_17) (or ?v_18 ?v_19) (or ?v_20 ?v_21) (or ?v_22 ?v_23) (or ?v_24 ?v_24) (not (p6 c15 c17)) (or ?v_0 ?v_82) (or ?v_2 ?v_97) (or ?v_5 ?v_112) (or ?v_10 ?v_127) (or ?v_17 ?v_142) (or ?v_1 ?v_85) (or ?v_3 ?v_100) (or ?v_7 ?v_115) (or ?v_12 ?v_130) (or ?v_19 ?v_145) (or ?v_4 ?v_88) (or ?v_6 ?v_103) (or ?v_8 ?v_118) (or ?v_14 ?v_133) (or ?v_21 ?v_148) (or ?v_9 ?v_91) (or ?v_11 ?v_106) (or ?v_13 ?v_121) (or ?v_15 ?v_136) (or ?v_23 ?v_151) (or ?v_16 ?v_94) (or ?v_18 ?v_109) (or ?v_20 ?v_124) (or ?v_22 ?v_139) (or ?v_24 ?v_154) (or ?v_155 ?v_25) (or ?v_156 ?v_26) (or ?v_157 ?v_27) (or ?v_158 ?v_28) (or ?v_159 ?v_29) (or ?v_160 ?v_30) (or ?v_161 ?v_31) (or ?v_162 ?v_32) (or ?v_163 ?v_33) (or ?v_164 ?v_34) (or ?v_165 ?v_35) (or ?v_166 ?v_36) (or ?v_167 ?v_37) (or ?v_168 ?v_38) (or ?v_169 ?v_39) (or ?v_170 ?v_40) (or ?v_171 ?v_41) (or ?v_172 ?v_42) (or ?v_173 ?v_43) (or ?v_174 ?v_44) (or ?v_175 ?v_45) (or ?v_176 ?v_46) (or ?v_177 ?v_47) (or ?v_178 ?v_48) (or ?v_179 ?v_49) (p4 c13 c11) (or ?v_0 ?v_50) (or ?v_2 ?v_51) (or ?v_5 ?v_52) (or ?v_10 ?v_53) (or ?v_17 ?v_54) (or ?v_1 ?v_55) (or ?v_3 ?v_56) (or ?v_7 ?v_57) (or ?v_12 ?v_58) (or ?v_19 ?v_59) (or ?v_4 ?v_60) (or ?v_6 ?v_61) (or ?v_8 ?v_62) (or ?v_14 ?v_63) (or ?v_21 ?v_64) (or ?v_9 ?v_65) (or ?v_11 ?v_66) (or ?v_13 ?v_67) (or ?v_15 ?v_68) (or ?v_23 ?v_69) (or ?v_16 ?v_70) (or ?v_18 ?v_71) (or ?v_20 ?v_72) (or ?v_22 ?v_73) (or ?v_24 ?v_74) (or (= ?v_181 c10) ?v_75 (not ?v_180)) (or (= ?v_183 c10) ?v_75 (not ?v_182)) (or (= ?v_185 c10) ?v_75 (not ?v_184)) (or (= ?v_187 c10) ?v_75 (not ?v_186)) (or (= ?v_189 c10) ?v_75 (not ?v_188)) (or (= ?v_191 c10) ?v_76 (not ?v_190)) (or (= ?v_193 c10) ?v_76 (not ?v_192)) (or (= ?v_195 c10) ?v_76 (not ?v_194)) (or (= ?v_197 c10) ?v_76 (not ?v_196)) (or (= ?v_199 c10) ?v_76 (not ?v_198)) (or (= ?v_201 c10) ?v_77 (not ?v_200)) (or (= ?v_203 c10) ?v_77 (not ?v_202)) (or (= ?v_205 c10) ?v_77 (not ?v_204)) (or (= ?v_207 c10) ?v_77 (not ?v_206)) (or (= ?v_209 c10) ?v_77 (not ?v_208)) (or (= ?v_211 c10) ?v_78 (not ?v_210)) (or (= ?v_213 c10) ?v_78 (not ?v_212)) (or (= ?v_215 c10) ?v_78 (not ?v_214)) (or (= ?v_217 c10) ?v_78 (not ?v_216)) (or (= ?v_219 c10) ?v_78 (not ?v_218)) (or (= ?v_221 c10) ?v_79 (not ?v_220)) (or (= ?v_223 c10) ?v_79 (not ?v_222)) (or (= ?v_225 c10) ?v_79 (not ?v_224)) (or (= ?v_227 c10) ?v_79 (not ?v_226)) (or (= ?v_229 c10) ?v_79 (not ?v_228)) (p6 c15 c16) (p8 c15) (not (p4 (f5 c15 c17) (f5 c15 c16))) (or ?v_80 ?v_81 ?v_82) (or ?v_83 ?v_84 ?v_85) (or ?v_86 ?v_87 ?v_88) (or ?v_89 ?v_90 ?v_91) (or ?v_92 ?v_93 ?v_94) (or ?v_95 ?v_96 ?v_97) (or ?v_98 ?v_99 ?v_100) (or ?v_101 ?v_102 ?v_103) (or ?v_104 ?v_105 ?v_106) (or ?v_107 ?v_108 ?v_109) (or ?v_110 ?v_111 ?v_112) (or ?v_113 ?v_114 ?v_115) (or ?v_116 ?v_117 ?v_118) (or ?v_119 ?v_120 ?v_121) (or ?v_122 ?v_123 ?v_124) (or ?v_125 ?v_126 ?v_127) (or ?v_128 ?v_129 ?v_130) (or ?v_131 ?v_132 ?v_133) (or ?v_134 ?v_135 ?v_136) (or ?v_137 ?v_138 ?v_139) (or ?v_140 ?v_141 ?v_142) (or ?v_143 ?v_144 ?v_145) (or ?v_146 ?v_147 ?v_148) (or ?v_149 ?v_150 ?v_151) (or ?v_152 ?v_153 ?v_154) (p4 c12 c11) (or ?v_80 (not ?v_155) ?v_82) (or ?v_83 (not ?v_156) ?v_85) (or ?v_86 (not ?v_157) ?v_88) (or ?v_89 (not ?v_158) ?v_91) (or ?v_92 (not ?v_159) ?v_94) (or ?v_95 (not ?v_160) ?v_97) (or ?v_98 (not ?v_161) ?v_100) (or ?v_101 (not ?v_162) ?v_103) (or ?v_104 (not ?v_163) ?v_106) (or ?v_107 (not ?v_164) ?v_109) (or ?v_110 (not ?v_165) ?v_112) (or ?v_113 (not ?v_166) ?v_115) (or ?v_116 (not ?v_167) ?v_118) (or ?v_119 (not ?v_168) ?v_121) (or ?v_122 (not ?v_169) ?v_124) (or ?v_125 (not ?v_170) ?v_127) (or ?v_128 (not ?v_171) ?v_130) (or ?v_131 (not ?v_172) ?v_133) (or ?v_134 (not ?v_173) ?v_136) (or ?v_137 (not ?v_174) ?v_139) (or ?v_140 (not ?v_175) ?v_142) (or ?v_143 (not ?v_176) ?v_145) (or ?v_146 (not ?v_177) ?v_148) (or ?v_149 (not ?v_178) ?v_151) (or ?v_152 (not ?v_179) ?v_154) (or ?v_81 ?v_230) (or ?v_84 ?v_235) (or ?v_87 ?v_240) (or ?v_90 ?v_245) (or ?v_93 ?v_250) (or ?v_96 ?v_231) (or ?v_99 ?v_236) (or ?v_102 ?v_241) (or ?v_105 ?v_246) (or ?v_108 ?v_251) (or ?v_111 ?v_232) (or ?v_114 ?v_237) (or ?v_117 ?v_242) (or ?v_120 ?v_247) (or ?v_123 ?v_252) (or ?v_126 ?v_233) (or ?v_129 ?v_238) (or ?v_132 ?v_243) (or ?v_135 ?v_248) (or ?v_138 ?v_253) (or ?v_141 ?v_234) (or ?v_144 ?v_239) (or ?v_147 ?v_244) (or ?v_150 ?v_249) (or ?v_153 ?v_254) (or ?v_80 ?v_81 (not ?v_50)) (or ?v_83 ?v_84 (not ?v_51)) (or ?v_86 ?v_87 (not ?v_52)) (or ?v_89 ?v_90 (not ?v_53)) (or ?v_92 ?v_93 (not ?v_54)) (or ?v_95 ?v_96 (not ?v_55)) (or ?v_98 ?v_99 (not ?v_56)) (or ?v_101 ?v_102 (not ?v_57)) (or ?v_104 ?v_105 (not ?v_58)) (or ?v_107 ?v_108 (not ?v_59)) (or ?v_110 ?v_111 (not ?v_60)) (or ?v_113 ?v_114 (not ?v_61)) (or ?v_116 ?v_117 (not ?v_62)) (or ?v_119 ?v_120 (not ?v_63)) (or ?v_122 ?v_123 (not ?v_64)) (or ?v_125 ?v_126 (not ?v_65)) (or ?v_128 ?v_129 (not ?v_66)) (or ?v_131 ?v_132 (not ?v_67)) (or ?v_134 ?v_135 (not ?v_68)) (or ?v_137 ?v_138 (not ?v_69)) (or ?v_140 ?v_141 (not ?v_70)) (or ?v_143 ?v_144 (not ?v_71)) (or ?v_146 ?v_147 (not ?v_72)) (or ?v_149 ?v_150 (not ?v_73)) (or ?v_152 ?v_153 (not ?v_74)) (p4 c11 c10) (or ?v_0 ?v_81 ?v_0) (or ?v_0 ?v_84 ?v_2) (or ?v_0 ?v_87 ?v_5) (or ?v_0 ?v_90 ?v_10) (or ?v_0 ?v_93 ?v_17) (or ?v_2 ?v_81 ?v_1) (or ?v_2 ?v_84 ?v_3) (or ?v_2 ?v_87 ?v_7) (or ?v_2 ?v_90 ?v_12) (or ?v_2 ?v_93 ?v_19) (or ?v_5 ?v_81 ?v_4) (or ?v_5 ?v_84 ?v_6) (or ?v_5 ?v_87 ?v_8) (or ?v_5 ?v_90 ?v_14) (or ?v_5 ?v_93 ?v_21) (or ?v_10 ?v_81 ?v_9) (or ?v_10 ?v_84 ?v_11) (or ?v_10 ?v_87 ?v_13) (or ?v_10 ?v_90 ?v_15) (or ?v_10 ?v_93 ?v_23) (or ?v_17 ?v_81 ?v_16) (or ?v_17 ?v_84 ?v_18) (or ?v_17 ?v_87 ?v_20) (or ?v_17 ?v_90 ?v_22) (or ?v_17 ?v_93 ?v_24) (or ?v_1 ?v_96 ?v_0) (or ?v_1 ?v_99 ?v_2) (or ?v_1 ?v_102 ?v_5) (or ?v_1 ?v_105 ?v_10) (or ?v_1 ?v_108 ?v_17) (or ?v_3 ?v_96 ?v_1) (or ?v_3 ?v_99 ?v_3) (or ?v_3 ?v_102 ?v_7) (or ?v_3 ?v_105 ?v_12) (or ?v_3 ?v_108 ?v_19) (or ?v_7 ?v_96 ?v_4) (or ?v_7 ?v_99 ?v_6) (or ?v_7 ?v_102 ?v_8) (or ?v_7 ?v_105 ?v_14) (or ?v_7 ?v_108 ?v_21) (or ?v_12 ?v_96 ?v_9) (or ?v_12 ?v_99 ?v_11) (or ?v_12 ?v_102 ?v_13) (or ?v_12 ?v_105 ?v_15) (or ?v_12 ?v_108 ?v_23) (or ?v_19 ?v_96 ?v_16) (or ?v_19 ?v_99 ?v_18) (or ?v_19 ?v_102 ?v_20) (or ?v_19 ?v_105 ?v_22) (or ?v_19 ?v_108 ?v_24) (or ?v_4 ?v_111 ?v_0) (or ?v_4 ?v_114 ?v_2) (or ?v_4 ?v_117 ?v_5) (or ?v_4 ?v_120 ?v_10) (or ?v_4 ?v_123 ?v_17) (or ?v_6 ?v_111 ?v_1) (or ?v_6 ?v_114 ?v_3) (or ?v_6 ?v_117 ?v_7) (or ?v_6 ?v_120 ?v_12) (or ?v_6 ?v_123 ?v_19) (or ?v_8 ?v_111 ?v_4) (or ?v_8 ?v_114 ?v_6) (or ?v_8 ?v_117 ?v_8) (or ?v_8 ?v_120 ?v_14) (or ?v_8 ?v_123 ?v_21) (or ?v_14 ?v_111 ?v_9) (or ?v_14 ?v_114 ?v_11) (or ?v_14 ?v_117 ?v_13) (or ?v_14 ?v_120 ?v_15) (or ?v_14 ?v_123 ?v_23) (or ?v_21 ?v_111 ?v_16) (or ?v_21 ?v_114 ?v_18) (or ?v_21 ?v_117 ?v_20) (or ?v_21 ?v_120 ?v_22) (or ?v_21 ?v_123 ?v_24) (or ?v_9 ?v_126 ?v_0) (or ?v_9 ?v_129 ?v_2) (or ?v_9 ?v_132 ?v_5) (or ?v_9 ?v_135 ?v_10) (or ?v_9 ?v_138 ?v_17) (or ?v_11 ?v_126 ?v_1) (or ?v_11 ?v_129 ?v_3) (or ?v_11 ?v_132 ?v_7) (or ?v_11 ?v_135 ?v_12) (or ?v_11 ?v_138 ?v_19) (or ?v_13 ?v_126 ?v_4) (or ?v_13 ?v_129 ?v_6) (or ?v_13 ?v_132 ?v_8) (or ?v_13 ?v_135 ?v_14) (or ?v_13 ?v_138 ?v_21) (or ?v_15 ?v_126 ?v_9) (or ?v_15 ?v_129 ?v_11) (or ?v_15 ?v_132 ?v_13) (or ?v_15 ?v_135 ?v_15) (or ?v_15 ?v_138 ?v_23) (or ?v_23 ?v_126 ?v_16) (or ?v_23 ?v_129 ?v_18) (or ?v_23 ?v_132 ?v_20) (or ?v_23 ?v_135 ?v_22) (or ?v_23 ?v_138 ?v_24) (or ?v_16 ?v_141 ?v_0) (or ?v_16 ?v_144 ?v_2) (or ?v_16 ?v_147 ?v_5) (or ?v_16 ?v_150 ?v_10) (or ?v_16 ?v_153 ?v_17) (or ?v_18 ?v_141 ?v_1) (or ?v_18 ?v_144 ?v_3) (or ?v_18 ?v_147 ?v_7) (or ?v_18 ?v_150 ?v_12) (or ?v_18 ?v_153 ?v_19) (or ?v_20 ?v_141 ?v_4) (or ?v_20 ?v_144 ?v_6) (or ?v_20 ?v_147 ?v_8) (or ?v_20 ?v_150 ?v_14) (or ?v_20 ?v_153 ?v_21) (or ?v_22 ?v_141 ?v_9) (or ?v_22 ?v_144 ?v_11) (or ?v_22 ?v_147 ?v_13) (or ?v_22 ?v_150 ?v_15) (or ?v_22 ?v_153 ?v_23) (or ?v_24 ?v_141 ?v_16) (or ?v_24 ?v_144 ?v_18) (or ?v_24 ?v_147 ?v_20) (or ?v_24 ?v_150 ?v_22) (or ?v_24 ?v_153 ?v_24) (or ?v_330 ?v_180 ?v_75 ?v_256 (= ?v_181 c11)) (or ?v_331 ?v_182 ?v_75 ?v_258 (= ?v_183 c11)) (or ?v_332 ?v_184 ?v_75 ?v_260 (= ?v_185 c11)) (or ?v_333 ?v_186 ?v_75 ?v_262 (= ?v_187 c11)) (or ?v_334 ?v_188 ?v_75 ?v_264 (= ?v_189 c11)) (or ?v_335 ?v_190 ?v_76 ?v_266 (= ?v_191 c11)) (or ?v_336 ?v_192 ?v_76 ?v_268 (= ?v_193 c11)) (or ?v_337 ?v_194 ?v_76 ?v_270 (= ?v_195 c11)) (or ?v_338 ?v_196 ?v_76 ?v_272 (= ?v_197 c11)) (or ?v_339 ?v_198 ?v_76 ?v_274 (= ?v_199 c11)) (or ?v_340 ?v_200 ?v_77 ?v_276 (= ?v_201 c11)) (or ?v_341 ?v_202 ?v_77 ?v_278 (= ?v_203 c11)) (or ?v_342 ?v_204 ?v_77 ?v_280 (= ?v_205 c11)) (or ?v_343 ?v_206 ?v_77 ?v_282 (= ?v_207 c11)) (or ?v_344 ?v_208 ?v_77 ?v_284 (= ?v_209 c11)) (or ?v_345 ?v_210 ?v_78 ?v_286 (= ?v_211 c11)) (or ?v_346 ?v_212 ?v_78 ?v_288 (= ?v_213 c11)) (or ?v_347 ?v_214 ?v_78 ?v_290 (= ?v_215 c11)) (or ?v_348 ?v_216 ?v_78 ?v_292 (= ?v_217 c11)) (or ?v_349 ?v_218 ?v_78 ?v_294 (= ?v_219 c11)) (or ?v_350 ?v_220 ?v_79 ?v_296 (= ?v_221 c11)) (or ?v_351 ?v_222 ?v_79 ?v_298 (= ?v_223 c11)) (or ?v_352 ?v_224 ?v_79 ?v_300 (= ?v_225 c11)) (or ?v_353 ?v_226 ?v_79 ?v_302 (= ?v_227 c11)) (or ?v_354 ?v_228 ?v_79 ?v_304 (= ?v_229 c11)) (or ?v_230 ?v_155) (or ?v_231 ?v_156) (or ?v_232 ?v_157) (or ?v_233 ?v_158) (or ?v_234 ?v_159) (or ?v_235 ?v_160) (or ?v_236 ?v_161) (or ?v_237 ?v_162) (or ?v_238 ?v_163) (or ?v_239 ?v_164) (or ?v_240 ?v_165) (or ?v_241 ?v_166) (or ?v_242 ?v_167) (or ?v_243 ?v_168) (or ?v_244 ?v_169) (or ?v_245 ?v_170) (or ?v_246 ?v_171) (or ?v_247 ?v_172) (or ?v_248 ?v_173) (or ?v_249 ?v_174) (or ?v_250 ?v_175) (or ?v_251 ?v_176) (or ?v_252 ?v_177) (or ?v_253 ?v_178) (or ?v_254 ?v_179) (or ?v_180 (= ?v_181 c13) ?v_255 ?v_75 ?v_256) (or ?v_182 (= ?v_183 c13) ?v_257 ?v_75 ?v_258) (or ?v_184 (= ?v_185 c13) ?v_259 ?v_75 ?v_260) (or ?v_186 (= ?v_187 c13) ?v_261 ?v_75 ?v_262) (or ?v_188 (= ?v_189 c13) ?v_263 ?v_75 ?v_264) (or ?v_190 (= ?v_191 c13) ?v_265 ?v_76 ?v_266) (or ?v_192 (= ?v_193 c13) ?v_267 ?v_76 ?v_268) (or ?v_194 (= ?v_195 c13) ?v_269 ?v_76 ?v_270) (or ?v_196 (= ?v_197 c13) ?v_271 ?v_76 ?v_272) (or ?v_198 (= ?v_199 c13) ?v_273 ?v_76 ?v_274) (or ?v_200 (= ?v_201 c13) ?v_275 ?v_77 ?v_276) (or ?v_202 (= ?v_203 c13) ?v_277 ?v_77 ?v_278) (or ?v_204 (= ?v_205 c13) ?v_279 ?v_77 ?v_280) (or ?v_206 (= ?v_207 c13) ?v_281 ?v_77 ?v_282) (or ?v_208 (= ?v_209 c13) ?v_283 ?v_77 ?v_284) (or ?v_210 (= ?v_211 c13) ?v_285 ?v_78 ?v_286) (or ?v_212 (= ?v_213 c13) ?v_287 ?v_78 ?v_288) (or ?v_214 (= ?v_215 c13) ?v_289 ?v_78 ?v_290) (or ?v_216 (= ?v_217 c13) ?v_291 ?v_78 ?v_292) (or ?v_218 (= ?v_219 c13) ?v_293 ?v_78 ?v_294) (or ?v_220 (= ?v_221 c13) ?v_295 ?v_79 ?v_296) (or ?v_222 (= ?v_223 c13) ?v_297 ?v_79 ?v_298) (or ?v_224 (= ?v_225 c13) ?v_299 ?v_79 ?v_300) (or ?v_226 (= ?v_227 c13) ?v_301 ?v_79 ?v_302) (or ?v_228 (= ?v_229 c13) ?v_303 ?v_79 ?v_304) (or (= ?v_181 c14) ?v_305 ?v_180 ?v_75 ?v_255) (or (= ?v_183 c14) ?v_306 ?v_182 ?v_75 ?v_257) (or (= ?v_185 c14) ?v_307 ?v_184 ?v_75 ?v_259) (or (= ?v_187 c14) ?v_308 ?v_186 ?v_75 ?v_261) (or (= ?v_189 c14) ?v_309 ?v_188 ?v_75 ?v_263) (or (= ?v_191 c14) ?v_310 ?v_190 ?v_76 ?v_265) (or (= ?v_193 c14) ?v_311 ?v_192 ?v_76 ?v_267) (or (= ?v_195 c14) ?v_312 ?v_194 ?v_76 ?v_269) (or (= ?v_197 c14) ?v_313 ?v_196 ?v_76 ?v_271) (or (= ?v_199 c14) ?v_314 ?v_198 ?v_76 ?v_273) (or (= ?v_201 c14) ?v_315 ?v_200 ?v_77 ?v_275) (or (= ?v_203 c14) ?v_316 ?v_202 ?v_77 ?v_277) (or (= ?v_205 c14) ?v_317 ?v_204 ?v_77 ?v_279) (or (= ?v_207 c14) ?v_318 ?v_206 ?v_77 ?v_281) (or (= ?v_209 c14) ?v_319 ?v_208 ?v_77 ?v_283) (or (= ?v_211 c14) ?v_320 ?v_210 ?v_78 ?v_285) (or (= ?v_213 c14) ?v_321 ?v_212 ?v_78 ?v_287) (or (= ?v_215 c14) ?v_322 ?v_214 ?v_78 ?v_289) (or (= ?v_217 c14) ?v_323 ?v_216 ?v_78 ?v_291) (or (= ?v_219 c14) ?v_324 ?v_218 ?v_78 ?v_293) (or (= ?v_221 c14) ?v_325 ?v_220 ?v_79 ?v_295) (or (= ?v_223 c14) ?v_326 ?v_222 ?v_79 ?v_297) (or (= ?v_225 c14) ?v_327 ?v_224 ?v_79 ?v_299) (or (= ?v_227 c14) ?v_328 ?v_226 ?v_79 ?v_301) (or (= ?v_229 c14) ?v_329 ?v_228 ?v_79 ?v_303) (or ?v_180 ?v_330 ?v_305 (= ?v_181 c12) ?v_75) (or ?v_182 ?v_331 ?v_306 (= ?v_183 c12) ?v_75) (or ?v_184 ?v_332 ?v_307 (= ?v_185 c12) ?v_75) (or ?v_186 ?v_333 ?v_308 (= ?v_187 c12) ?v_75) (or ?v_188 ?v_334 ?v_309 (= ?v_189 c12) ?v_75) (or ?v_190 ?v_335 ?v_310 (= ?v_191 c12) ?v_76) (or ?v_192 ?v_336 ?v_311 (= ?v_193 c12) ?v_76) (or ?v_194 ?v_337 ?v_312 (= ?v_195 c12) ?v_76) (or ?v_196 ?v_338 ?v_313 (= ?v_197 c12) ?v_76) (or ?v_198 ?v_339 ?v_314 (= ?v_199 c12) ?v_76) (or ?v_200 ?v_340 ?v_315 (= ?v_201 c12) ?v_77) (or ?v_202 ?v_341 ?v_316 (= ?v_203 c12) ?v_77) (or ?v_204 ?v_342 ?v_317 (= ?v_205 c12) ?v_77) (or ?v_206 ?v_343 ?v_318 (= ?v_207 c12) ?v_77) (or ?v_208 ?v_344 ?v_319 (= ?v_209 c12) ?v_77) (or ?v_210 ?v_345 ?v_320 (= ?v_211 c12) ?v_78) (or ?v_212 ?v_346 ?v_321 (= ?v_213 c12) ?v_78) (or ?v_214 ?v_347 ?v_322 (= ?v_215 c12) ?v_78) (or ?v_216 ?v_348 ?v_323 (= ?v_217 c12) ?v_78) (or ?v_218 ?v_349 ?v_324 (= ?v_219 c12) ?v_78) (or ?v_220 ?v_350 ?v_325 (= ?v_221 c12) ?v_79) (or ?v_222 ?v_351 ?v_326 (= ?v_223 c12) ?v_79) (or ?v_224 ?v_352 ?v_327 (= ?v_225 c12) ?v_79) (or ?v_226 ?v_353 ?v_328 (= ?v_227 c12) ?v_79) (or ?v_228 ?v_354 ?v_329 (= ?v_229 c12) ?v_79) (or (= ?v_181 c_0) (= ?v_181 c_1) (= ?v_181 c_2) (= ?v_181 c_3) (= ?v_181 c_4)) (or (= ?v_183 c_0) (= ?v_183 c_1) (= ?v_183 c_2) (= ?v_183 c_3) (= ?v_183 c_4)) (or (= ?v_185 c_0) (= ?v_185 c_1) (= ?v_185 c_2) (= ?v_185 c_3) (= ?v_185 c_4)) (or (= ?v_187 c_0) (= ?v_187 c_1) (= ?v_187 c_2) (= ?v_187 c_3) (= ?v_187 c_4)) (or (= ?v_189 c_0) (= ?v_189 c_1) (= ?v_189 c_2) (= ?v_189 c_3) (= ?v_189 c_4)) (or (= ?v_191 c_0) (= ?v_191 c_1) (= ?v_191 c_2) (= ?v_191 c_3) (= ?v_191 c_4)) (or (= ?v_193 c_0) (= ?v_193 c_1) (= ?v_193 c_2) (= ?v_193 c_3) (= ?v_193 c_4)) (or (= ?v_195 c_0) (= ?v_195 c_1) (= ?v_195 c_2) (= ?v_195 c_3) (= ?v_195 c_4)) (or (= ?v_197 c_0) (= ?v_197 c_1) (= ?v_197 c_2) (= ?v_197 c_3) (= ?v_197 c_4)) (or (= ?v_199 c_0) (= ?v_199 c_1) (= ?v_199 c_2) (= ?v_199 c_3) (= ?v_199 c_4)) (or (= ?v_201 c_0) (= ?v_201 c_1) (= ?v_201 c_2) (= ?v_201 c_3) (= ?v_201 c_4)) (or (= ?v_203 c_0) (= ?v_203 c_1) (= ?v_203 c_2) (= ?v_203 c_3) (= ?v_203 c_4)) (or (= ?v_205 c_0) (= ?v_205 c_1) (= ?v_205 c_2) (= ?v_205 c_3) (= ?v_205 c_4)) (or (= ?v_207 c_0) (= ?v_207 c_1) (= ?v_207 c_2) (= ?v_207 c_3) (= ?v_207 c_4)) (or (= ?v_209 c_0) (= ?v_209 c_1) (= ?v_209 c_2) (= ?v_209 c_3) (= ?v_209 c_4)) (or (= ?v_211 c_0) (= ?v_211 c_1) (= ?v_211 c_2) (= ?v_211 c_3) (= ?v_211 c_4)) (or (= ?v_213 c_0) (= ?v_213 c_1) (= ?v_213 c_2) (= ?v_213 c_3) (= ?v_213 c_4)) (or (= ?v_215 c_0) (= ?v_215 c_1) (= ?v_215 c_2) (= ?v_215 c_3) (= ?v_215 c_4)) (or (= ?v_217 c_0) (= ?v_217 c_1) (= ?v_217 c_2) (= ?v_217 c_3) (= ?v_217 c_4)) (or (= ?v_219 c_0) (= ?v_219 c_1) (= ?v_219 c_2) (= ?v_219 c_3) (= ?v_219 c_4)) (or (= ?v_221 c_0) (= ?v_221 c_1) (= ?v_221 c_2) (= ?v_221 c_3) (= ?v_221 c_4)) (or (= ?v_223 c_0) (= ?v_223 c_1) (= ?v_223 c_2) (= ?v_223 c_3) (= ?v_223 c_4)) (or (= ?v_225 c_0) (= ?v_225 c_1) (= ?v_225 c_2) (= ?v_225 c_3) (= ?v_225 c_4)) (or (= ?v_227 c_0) (= ?v_227 c_1) (= ?v_227 c_2) (= ?v_227 c_3) (= ?v_227 c_4)) (or (= ?v_229 c_0) (= ?v_229 c_1) (= ?v_229 c_2) (= ?v_229 c_3) (= ?v_229 c_4)) (or (= c14 c_0) (= c14 c_1) (= c14 c_2) (= c14 c_3) (= c14 c_4)) (or (= c12 c_0) (= c12 c_1) (= c12 c_2) (= c12 c_3) (= c12 c_4)) (or (= c13 c_0) (= c13 c_1) (= c13 c_2) (= c13 c_3) (= c13 c_4)) (or (= c15 c_0) (= c15 c_1) (= c15 c_2) (= c15 c_3) (= c15 c_4)) (or (= c17 c_0) (= c17 c_1) (= c17 c_2) (= c17 c_3) (= c17 c_4)) (or (= c11 c_0) (= c11 c_1) (= c11 c_2) (= c11 c_3) (= c11 c_4)) (or (= c10 c_0) (= c10 c_1) (= c10 c_2) (= c10 c_3) (= c10 c_4)) (or (= c16 c_0) (= c16 c_1) (= c16 c_2) (= c16 c_3) (= c16 c_4))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(exit)
